msg{-}item(${\it ds}$;${\it da}$;$k$;$l$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it tg}$:Id$\times\mathbb{N}\times$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$(${\it da}$(rcv($l$,${\it tg}$))?Void List))